\begin{tabbing}
inv{-}rel($A$;$B$;$f$;${\it finv}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$a$:$A$, $b$:$B$. ${\it finv}$($b$) $=$ inl($a$) $\in$ $A$+Unit $\Rightarrow$ $b$ $=$ $f$($a$) $\in$ $B$)\+
\\[0ex]\& ($\forall$$a$:$A$. ${\it finv}$($f$($a$)) $=$ inl($a$) $\in$ $A$+Unit)
\-
\end{tabbing}